/*
 * Kodkod -- Copyright (c) 2005-present, Emina Torlak
 *
 * Permission is hereby granted, free of charge, to any person obtaining a copy
 * of this software and associated documentation files (the "Software"), to deal
 * in the Software without restriction, including without limitation the rights
 * to use, copy, modify, merge, publish, distribute, sublicense, and/or sell
 * copies of the Software, and to permit persons to whom the Software is
 * furnished to do so, subject to the following conditions:
 *
 * The above copyright notice and this permission notice shall be included in
 * all copies or substantial portions of the Software.
 *
 * THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
 * IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
 * FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
 * AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
 * LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM,
 * OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN
 * THE SOFTWARE.
 */
package kodkod.engine.ucore;

import java.util.Iterator;

import kodkod.engine.fol2sat.TranslationLog;
import kodkod.engine.fol2sat.Translator;
import kodkod.engine.satlab.Clause;
import kodkod.engine.satlab.ReductionStrategy;
import kodkod.engine.satlab.ResolutionTrace;
import kodkod.util.ints.IntBitSet;
import kodkod.util.ints.IntIterator;
import kodkod.util.ints.IntSet;
import kodkod.util.ints.Ints;

/**
 * A hybrid strategy for generating unsat cores that are minimal when mapped
 * back onto the logic level. Specifically, let C be a core that is minimal
 * according to this strategy, and let F(C) be the top-level logic constraints
 * corresponding to C. Then, this strategy guarantees that there is no clause c
 * in C such that F(C - c) is a strict subset of F(C). Note that this does not
 * guarantee that F(C) itself is minimal. In other words, there could be an f in
 * F(C) such that F(C) - f is unsatisfiable. To get a minimal logic core, use
 * {@linkplain RCEStrategy}.
 * <p>
 * This strategy will work properly only on CNFs generated by the kodkod
 * {@linkplain Translator}.
 * </p>
 *
 * @author Emina Torlak
 * @see RCEStrategy
 */
public final class HybridStrategy implements ReductionStrategy {

    private final IntSet topVars;

    /**
     * Constructs a hybrid strategy that will use the given translation log to
     * relate the cnf clauses back to the logic constraints from which they were
     * generated.
     */
    public HybridStrategy(TranslationLog log) {
        topVars = StrategyUtils.rootVars(log);
    }

    /**
     * {@inheritDoc}
     *
     * @see kodkod.engine.satlab.ReductionStrategy#next(kodkod.engine.satlab.ResolutionTrace)
     */
    @Override
    public IntSet next(ResolutionTrace trace) {
        if (topVars.isEmpty())
            return Ints.EMPTY_SET; // tried everything
        final IntSet core = trace.core();

        for (Iterator<Clause> iter = trace.iterator(core); iter.hasNext();) {
            Clause clause = iter.next();
            int maxVar = clause.maxVariable();
            if (topVars.remove(maxVar)) {
                // get all core clauses with the given maximum variable
                IntSet exclude = coreClausesWithMaxVar(trace, maxVar);
                assert !exclude.isEmpty();
                // get all clauses reachable from the conflict clause
                IntSet next = trace.reachable(Ints.singleton(trace.size() - 1));
                // remove all clauses backward reachable from the clauses with
                // the given maxVar
                next.removeAll(trace.backwardReachable(exclude));
                if (!next.isEmpty()) {
                    return next;
                }
            }
        }

        topVars.clear();
        return Ints.EMPTY_SET;
    }

    /**
     * Returns the indices of the clauses in the unsatisfiable core of the given
     * trace that have the specified maximum variable.
     *
     * @return { i: trace.core() | trace[i].maxVariable() = maxVariable }
     */
    private static IntSet coreClausesWithMaxVar(ResolutionTrace trace, int maxVariable) {
        final IntSet core = trace.core();
        final IntSet restricted = new IntBitSet(core.max() + 1);
        final Iterator<Clause> clauses = trace.iterator(core);
        final IntIterator indices = core.iterator();
        while (clauses.hasNext()) {
            Clause clause = clauses.next();
            int index = indices.next();
            if (clause.maxVariable() == maxVariable)
                restricted.add(index);
        }
        return restricted;
    }

}
